$\forall$$X$:Type, ${\it eq}$:EqDecider($X$), $f$, $g$:$x$:$X$ fp$\rightarrow$ Type, $x$:$X$. \\[0ex]$f$ $\parallel$ $g$ $\Rightarrow$ $f$($x$)?Void $\Rightarrow$ $g$($x$)?Void $\Rightarrow$ ($f$($x$)?Void = $g$($x$)?Void $\in$ Type)